A, A':Type.
strong-subtype(A;A')
(B:(A
Type), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'), f, g:a:A fp B(a).
(a:A. B(a) 
r C(a)) {f g f g}) | 11,40 |
A, A':Type.
(B:(AType), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'), f, g:a:A fp B(a).
(a:A. B(a) r C(a)) {f g f g})
| Definitions | |
| Lemmas |